| Definitions | Top, State(ds), Y, ff, reduce(f;k;as), if b then t else f fi , f(x)?z, M.da(a), z != f(x)   P(a;z), f(x), M.state, deq-member(eq;x;L), x  dom(f),  b, M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), P Q, M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a),  , mk-ma, t.2, t.1,  xdom(f). v=f(x) P(x;v), P & Q, only members of L read x, k sends only on links in L, k affects only members of L, (precondition a:Outcome(p) is P:State(ds) -> Bool), with declarations ds:dsda:dak(v) sends f s v on link l, x : v, with declarations ds:dsda:daeffect of k(v) is x := f s v, only L sends on (l with tg), only members of L affect x :t, x : t initially x = v, ,   x. t(x), t T, R-base-ma(R), ma-frame-compat(A;B), x:A. B(x), False, x(s), Unit, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right,  , Rnone(),  |